
{
  open Lexing
  open Parser

  (* Used to count keywords *)
  let counts = Hashtbl.create 70

  (* Lexical errors *)
  exception Lexical_error of string

  (* Identifiers and Murphi keywords *)
  let id_or_keyword =
    let h = Hashtbl.create 70 in
    List.iter (fun (s, k) -> Hashtbl.add h s k)
      [ "array", ARRAY;
        "await", AWAIT;
        "int", INT;
        "bool", BOOL;
        "proc", PROC;
        "number_procs", NUMPROC;
        "process", PROCESS;
        "assert", ASSERT;
        "proccnt", PROCCNT;
        "is_zero", ISZERO;
        "not_zero", NOTZERO;
        "decr", DECR;
        "current", CURRENT;
        "atomic", ATOMIC;
        "true", TRUE;
        "false", FALSE;
        "endatom", ENDATOM;
        "const", CONST;
        "critical", CRITICAL;
        "else", ELSE;
        "forall_other", FORALL_OTHER;
        "exists_other", EXISTS_OTHER;
        "type", TYPE;
        "end", END;
        "endif", ENDIF;
        "for", FOR;
        "do", DO;
        "done", DONE;
        "to", TO;
        "var", VAR;
        "then", THEN;
        "if", IF;
        "return", RETURN;
        "while", WHILE ];
(*    fun s -> try Hashtbl.find h s with Not_found -> ID s *)
    fun s ->
	try
            let kw = (String.lowercase s) in
	    let t = Hashtbl.find h kw in
            begin try
                let c = Hashtbl.find counts kw in
	        Hashtbl.replace counts kw (c + 1)
            with Not_found -> Hashtbl.replace counts kw 1 end;
            t
	with Not_found -> IDENT s

 
  (* Newline handling *)
  let newline lexbuf =
    let pos = lexbuf.lex_curr_p in
    lexbuf.lex_curr_p <-
      { pos with
          pos_lnum = pos.pos_lnum + 1;
          pos_bol = pos.pos_cnum;
          pos_cnum = 0 }
}

let letter = ['a'-'z' 'A'-'Z' '_']
let uletter = ['A'-'Z' '_']
let lletter = ['A'-'Z' '_']
let digit = ['0'-'9']
let real = digit+ '.' digit*
let lident = letter (letter | digit)*
let uident = uletter (letter | digit)*
let str = '"' [^ '"' '\n']* '"'
let procnum = '#' digit+

rule token = parse
| "//" [^'\n']* ('\n' | eof) { newline lexbuf; token lexbuf }
| "(*"			{ comment lexbuf; token lexbuf }
| '\n'			{ newline lexbuf; token lexbuf }
| [' ' '\t' '\r']	{ token lexbuf }
| ".."			{ DOTDOT }
| "==>"			{ LONGARROW }
| "->"			{ IMPLIES }
| ":="			{ ASSIGN }
| '.'			{ DOT }
| ','			{ COMMA }
| ';'			{ SC }
| '{'			{ LCB }
| '}'			{ RCB }
| '['			{ LSB }
| ']'			{ RSB }
| '('			{ LP }
| ')'			{ RP }
| '&'			{ AMP }
| "&&"			{ AMPAMP }
| "||"			{ BARBAR }
| "|"			{ BAR }
| '!'			{ NOT }
| '?'			{ QM }
| ':'			{ COL }
| '='			{ EQ }
| "<>"			{ NEQ }
| "<="			{ LEQ }
| ">="			{ GEQ }
| '<'			{ LT }
| '>'			{ GT }
| '+'			{ PLUS }
| '-'			{ MINUS }
| '*'			{ TIMES }
| '/'			{ DIV }
| '%'			{ MOD }
| procnum as s		{ IDENT s }
| uident as s		{ MIDENT s }
| lident as s		{ id_or_keyword s }
| str	as s		{ STRING (s) }
| real as s
  {
    try REALCONST (float_of_string s)
    with _ -> raise (Lexical_error ("Invalid real constant : '" ^ s ^ "'"))
  }
| digit+ as s
  {
    try INTCONST (Int32.of_string s)
    with _ -> raise (Lexical_error ("Invalid integer constant : '" ^ s ^ "'"))
  }
| eof			{ EOF }
| _			{ raise (Lexical_error ("Illegal character : " ^ lexeme lexbuf)) }

(* Multi-line comment handling *)
and comment = parse
| "*)" { () }
| '\n' { newline lexbuf; comment lexbuf }
| eof  { raise (Lexical_error "Unterminated comment") }
| _    { comment lexbuf }

